.NH
Tokio: Temporal Logic as a Logic Programming Language 
.PP
As mentioned in the previous chapter, behaviors of hardwares are
easily described in LTTL with interval signals.
Here we present a logic programming language: Tokio,
which is based upon first order LTTL, and its interpreter,
which can directly execute Tokio programs.
The name of Tokio comes from the Japanese 'toki (time) o kakeru gengo',
which means 'a language that describes time and runs through time'.
In this chapter, we briefly introduce Tokio and 
show how to execute its programs.
The interpreter enables us to directly execute specifications written  in Tokio,
and has much practical importance.
Tokio is very similar to Tempura, which is based upon Interval temporal 
logic (ITL) and was developed by Moszkowski [7], and can be regarded as a 
logic-programming-version of Tempura.
Tokio is, however, strongly related to LTTL.
This enables us to directly apply our verification and synthesis techniques
to Tokio programs.
.NH 2
LTTL, Interval and Tokio
.PP
In this section, the logic of Tokio is discussed.
First, consider the interpretation of Tokio.
Meanings in Tokio are determined for interval variables. 
As mentioned earlier, there are three interval variables;
1) Ip, 2) Ip.beg, 3) Ip.fin,
which are all LTTL variables.
Interval is a finite sequence of unit time. 
To specify the interval, Ip itself is enough.
In order to bring the notion of interval into LTTL,
we associate with each interval a variable Ip for predicate p,
which indicates precisely the period
when the interval is active and whose predicate name is used as
the interval's name.
A pair Ip.beg and Ip.fin can be used instead of Ip.
They are unit pulses which indicate the beginning and end of Ip.
Since temporal logic handles only discrete time expressed with integers,
Ip.beg and Ip.fin corresponds to integers, i.e. absolute time.
Using pairs of interval variables,
we can describe an interval as <Ip.beg, Ip.fin>.
Moreover, we simply write an interval as <beg, fin> where beg and fin 
are integers as long as no confusion occurs.
Note that Ip.fin is greater or equal to Ip.beg. 
Though the meaning of a Tokio's predicate is determined for interval variables,
Tokio variables are still LTTL variable, i.e.
values of variables are defined for state.
In Tokio a state is a mapped to Ip.beg.
The value of a variable is determined at the beginning of the interval.
This corresponds to locality of variable in ITL [7].
.PP
The relationship between Tokio and first order LTTL is just like the one between
Prolog and first order predicate logic.
If we do not use temporal operators, the execution of Tokio is just the
same as that of Prolog.  
The syntax of Dec-10 Prolog is chosen here [10].
.IP examples
.br
.nf
ap([],X,X).                               (25)
ap([H|X],Y,[H|Z]) :- ap(X,Y,Z).           (26)
.fi
.LP
This is a Prolog append program. [X|Y] means a cons pair and []
means nil. 
A form 'ap(...)' is called a predicate. 
Variables in Tokio are words beginning with capital letters or '_'.
(25) is called a fact, and asserts some fact. This fact is true for
all <beg, fin>.
(26) consists of two parts, head and body, 
and implies that the body 
(to te right of ':-') must be satisfied in order to satisfy the head
(left of the ':-') for all <beg, fin>.
The interval variables of the body as same as head.
.PP
The Tokio program: 'p1, p2, ..., pn' is true in the 
interval <int.beg, int.fin> is described as:
.IP
int :- p1, p2, ..., pn.
.LP
That is, the interval name is used as a predicate name, and p1, 
p2, ..., pn are used as bodies.
.PP
The Horn clause in Tokio is extended with temporal operators.
In Tokio text, the prefix functor '@' means the 'next' function in LTTL.
.IP examples
.br
In an interval <beg, fin>,
.nf
A ........ value of variable A in <beg, fin>, 
@A ....... value of variable A in <beg+1, fin>,
           where fin is arbitrary,      (27)
A = 1 .... value of variable A at the current state is 1,
@A = 1 ... value of variable A in the next state is 1.
.fi
.LP
The '=' predicate is a special predicate in Tokio.
This is the only operator which selects current value of variable.
The meanings of @A = c with interval <Ip.beg, Ip.fin>
can be defined using the 'next' operator of LTTL as [](Ip.beg -> o (A = c))), 
.PP
The next statement means that A is incremented by 1.
.IP
@A = A+1       (28)
.LP
Like other logic programming
languages, values of variables in a fixed interval are assigned only once.
So we cannot write 
.IP
A = A+1.        (29)
.LP
This is a contradiction.
.NH 2
Interval generator 
  -- next, always and chop
.PP
There are many useful operators in ITL.
Here, three main operators in ITL are introduced to Tokio.
The execution of Tokio corresponds to viewing 
all intervals by incrementing time. 
For example,
at the time 'now', only the intervals where the beginning time is 'now',
such as, <now, fin>  <now,fin'>, ..., are evaluated.
Intervals <now+1,fin> are evaluated next. 
Interval generators are temporal operators which generate new intervals to be
evaluated.
An intervals disappears at the current time equals the ending of that interval.
The execution of a program continues until there are no intervals left to be 
evaluated, that is, when the ending times of all intervals have been reached.
We only admit finite intervals in Tokio.
.PP
First we introduce the operator 'next', '@'. 
We introduced this operator that gets the next value of a variable
in the previous section. 
But what does @p mean if p is a predicate?
If we meet @p in the interval <beg, fin>,
then p is true in the interval <beg+1, fin>,
that is, p is true at the next state. If beg+1>fin then interval 
<beg+1, fin> has no meaning. In such a case, @p is false.
This type of 'next' operator is called 'strong next' in ITL.
@ is a simple operator which generates <beg+1, fin> interval from <beg, fin>.
.IP examples 
.br
\'?-' means goal clause. 
.IP 
 ?-write(1).
 1
 yes
.LP
The 'write' statement simply writes its argument.
.IP
 ?-@write(2),write(1).
 12
 yes
.LP
A comma implies conjunction. 
Notice that 'write(1)' is executed first.
.PP
The second operator we introduce 
here is 'chop', '&&'.
In [7,8,9], ';' is the symbol for chop that has the same meanings as our '&&', 
but to avoid confusion with Prolog's 'or', ';',
we use '&&'. 
p\ &&\ q means the splitting of an interval into two subintervals.
p is executed in the former subinterval and q is executed in the 
later subinterval.
Or we can say simply "Do p. If p terminates then do q" just like the Pascal 
statement (22) of section 2.2.
The chop operator
generates two intervals <beg, mid>,<mid, fin> from interval <beg, fin>. 
LTTL can also express the chop operator; however,
it needs extra variables to distinguish
former and later intervals.
That is, <I.beg, I.fin> is divided into <I_former.beg, I_former.fin> and
<I_latter.beg, I_latter.fin>,
and interval variables must satisfy the following expressions:
.IP
.nf
I.beg <-> I_former.beg,
I.fin <-> I_latter.fin,          (30)
I_former.fin <-> I_latter.beg.
.fi
.LP
\'<->' is a logical equivalent.
I_former and I_latter are created by an existential quantifier.
In order to formally reason about Tokio programs, interval variables must be
indicated explicitly.
However, the actual execution does not need interval names, so we can 
omit them.
.PP
The last operator that generates intervals is the 'always' operator. 
It is expressed as '#'.
The 'always operator generates all subintervals
whose ending time coincides with
that of the original interval.
For example, <0,3>,<1,3>,<2,3>,<3,3> are generated from the interval <0,3>.
The '#' operator corresponds to LTTL''s square.
.IP example 
.br
 ?-length(5),#write(1).
 111111
 yes
.in 0
Length statement creates the interval <0,5>.
The 'always' operator generates <0,0>,
<1,5>,<2,5>,<3,5>,<4,5> and <5,5>. 
In these subintervals, 'write(1)' is executed.
.in 5
 ?-length(8),(length(5),#write(0) && #write(1)).
 0000001111
 yes
.in 0
First <0,8> is created. 
Then the 'chop' operator divides it into <0,5> and <5,8>. 
.NH 2
Basic predicates 
 -- empty, halt, fin, keep, stable, gets and ->
.PP  
To simplify descriptions, we need conditional statements. 
They are all ITL operators [7].
Operators such as 'empty', 'halt', 'fin', 'keep', 'stable',
'gets' and '->' are
introduced for this purpose.
In Tokio to
three conditional statements are available
for the control of interval length. 
In the following expressions, empty means length(0).
.IP
.nf
fin(p) :- #(    empty -> p).
keep(p):- #(not empty -> p).      (31)
halt(p):- #(p -> empty, not p -> not empty).
.fi
.LP
Though logical imply is
used as a condition, it contains negation that is difficult to execute
with interpreters.
Our definition of the if-statement should be directly executable
by Tokio interpreter, and so if-statement is not defined with negation 
and logical or. 
They are implemented using an extra logical operator called 'cut' i.e.
negation as failure [10].
.IP examples
.nf
A gets B :- keep(@A=B).
.br
?- A=1,A gets A+1,#write(A),length(4).
12345
yes
.fi
.LP
In the last instance of time in the interval we should not transfer A's value to
next A's value because there is no next time. 
Notice that 'A=1' is executed only once in the interval <0,4>,
because of the locality of predicate and variable.
.IP
.nf
?- A=0,A gets A+1,halt(A=4),#write(A).
01234
yes
.fi
.LP
This is an implementation of 'length'.
.IP
stable(A) :- A gets A.     (32)
.LP
This predicate indicates that A has the same value throughout the interval.
Next we show temporal assignment.
.IP
A<-B :- C=B,stable(C),fin(A=C).     (33)
.LP
B's value in the beginning time of the interval 
is transferred to the value of
A in the last time of the interval.
.IP
.nf
?- A=1, B=2, A<-B, B<-A, #write((A,B)),#nl, length(1).
1,2
2,1
yes
\'nl' writes newline.
.fi
.LP
The value of A and B is exchanged.
.NH 2 Examples of Tokio
.PP
We are now prepared to see how Tokio programs are used for hardware designs.
Figure (8) is an algorithm for asynchronous calculation
of magnitude of a two dimensional vector.
A and B are components of the vector.
|| means absolute value.
The algorithm is described in Tokio in Figure (9).
This is a rather procedural description similar to one written in Pascal or C,
and does not use interval variables. 
In this program, main interval is divided into
four subintervals and only in the first subinterval two calculations of
absolute are executed in parallel.
Figure (10) is an execution example.
This sequential implementation has flexible timing. 
.PP
To reason about this program, interval variables or interval names
should be added.
We indicate interval names by the predicate's name, i.e., the head.
The resulted program of adding interval names to Figure (9)
is shown in Figure (11).
The main interval 'magasync' is divided into four intervals, int1,
int2, int3 and int4.
.PP
As a next stage of hardware description, this algorithm can be executed
in a pipelined manner.
Figure (12) is its data path. The elements of the data path
have to to work synchronously.
In Figure (12) using always '#' and 
Tokio's primitive clock, it is described simply and easily. 
And this description is not procedural, but declarative. 
If we need more clocks in the 'calculation' part,
it means the need of internal 
pipelining or other synchronizing methods such as busy wait. 
Notice that the 'delay' part is the simplest way 
of synchronizing data flow. 
It does not need colored tokens, etc..
Figure (13) is an execution example. 
Predicate 'input' creats  data according to clock increment. 
The examples demonstrate that the pipelined execution proceeds correctly.
